(* # ===================================================================
   # Matrix Project
   # Copyright FEM-NUAA.CN 2020
   # =================================================================== *)


Require Import Reals.
Open Scope R_scope.
Require Export Matrix.Mat.RMatrix.
Require Export Matrix.Mat.RMtacs.

(** Sg -> Sa *)
(*
  地面坐标轴系Sg与气流坐标轴系Sa间的关系
  Sg在水平面转动φ度 得到过度坐标轴系S'，再在飞机对称面转动μ度得到过度坐标轴系S''，
  最后在OX''Y''面转动γ度得到气流坐标轴系Sa
*)

(* φ   *)
Parameter phi   : R.

(* μ   *)
Parameter my    : R.

(* γ  *)
Parameter gamma : R.


(* 由地面坐标轴系Sg 在水平面转动 φ 度 到 过度坐标轴系S’ *)
Definition coordinate_SgS' :  Mat R 3 3 := mkMat_3_3
  (cos phi) (sin phi) 0
  (-sin phi)(cos phi) 0
      0         0     1.

(* 由过度坐标轴系S’ 飞机对称面转动 μ度  到 过度坐标轴系S'' *)
Definition coordinate_S'S'' : Mat R 3 3 := mkMat_3_3
  (cos my )   0   (-sin my)
     0        1      0
  (sin my )   0   (cos my ).

(* 由过度坐标轴系S’’ 在OZ''Y''面转动 γ度  到 气流坐标轴系Sa *)

Definition coordinate_S''Sa : Mat R 3 3 := mkMat_3_3
  1           0            0
  0     (cos gamma)   (sin gamma)
  0     (-sin gamma)  (cos gamma).
(* 最后得到   地面坐标轴系Sg  到 气流坐标轴系Sa  转换 *)
Definition coordinate_SgSa : Mat R 3 3 := mkMat_3_3
  ((cos my)*(cos phi))  ((cos my)*(sin phi)) (-sin my)
  ((sin my)*(cos phi)*(sin gamma)-(sin phi)*(cos gamma)) 
  ((sin my)*(sin phi)*(sin gamma)+(cos phi)*(cos gamma)) 
  ((cos my)*(sin gamma))
  ((sin my)*(cos phi)*(cos gamma)+(sin phi)*(sin gamma)) 
  ((sin my)*(sin phi)*(cos gamma)-(cos phi)*(sin gamma)) 
  ((cos my)*(cos gamma)).

Definition transition_S''Sa_mul_S'S'' : Mat R 3 3 := mkMat_3_3
  (cos my)                       0          (-sin my)
  ((sin gamma)*(sin my))  (cos gamma)   ((sin gamma)*(cos my))
  ((cos gamma)*(sin my))  (-sin gamma)  ((cos gamma)*(cos my)).

Lemma transition_S'S''_mul_SgS'_eq:
  transition_S''Sa_mul_S'S'' === RMmul coordinate_S''Sa coordinate_S'S''.
Proof.
  unfold transition_S''Sa_mul_S'S''.
  RMat_mul_simpl. unfold mkMat_3_3'.
  f_equal3. 
Qed.

(* S''Sa * S'S'' * SgS' = S''Sa_mul_S'S'' * SgS' *)
Definition transition_S''Sa_mul_S'S''_mul_SgS' :=
  RMmul transition_S''Sa_mul_S'S'' coordinate_SgS'.


(* verify  S''Sa * S'S'' * SgS' = SgSa *)
Lemma coordinate_transform_SgSa_eq :
  coordinate_SgSa === transition_S''Sa_mul_S'S''_mul_SgS'.
Proof.
  unfold coordinate_SgSa.
  unfold transition_S''Sa_mul_S'S''_mul_SgS'.
  RMat_mul_simpl. unfold mkMat_3_3'.
  f_equal3. ring. f_equal2. ring. ring. ring.
  f_equal2. ring. ring. ring. f_equal. ring.
Qed.

